Univalent Foundations
Univalent foundations
ホモトピー型理論(Homotopy Type Theory(HoTT))のやつ
Martin-Löf型理論 + ホモトピー論
Univalence Axiom (UA)を基礎として数学を再構成するためのもの
ZFC公理系、圏論のような数学の基礎として扱うような理論[Thierry2014]
Voevodskyが作った
メタ理論といえるらしい
現在はUnivalent Foundationの実装がUniMathに含まれている
定理証明支援系によってはうまく実装ができないためCubical Type Theory、Observational Type Theoryでうまく形式化できる道が模索されている
Univalent Foundationsの訳
Univalent
一価の or 同値性の
foundations
基礎付けが良さそう
Voevodskyのページ: Univalent Foundations of Mathematics
Univalent foundationができた経緯の記事。
The Origins and Motivations of Univalent Foundations - Ideas | Institute for Advanced Study. 2014.
Univalent FoundationsについてのVoevodskyのインタビュー
Интервью Владимира Воеводского (часть 1). 2012-07-01.
確認用
Q. Univalent foundation
関連
Homotopy Type Theory(HoTT)
Martin-Löf型理論
Univalence Axiom (UA)
h-level
参考
Univalent foundations - Wikipedia
証明へのコンピュータの利用 -- Univalent Foundation - YouTube
証明へのコンピュータの利用(pdf)
「正しい」圏論
[Thierry2014] Thierry Coquand. Univalent Foundation and Constructive Mathematics. 2014-11-21
メモ
Univalent Foundations of Mathematics - Program Description - School of Mathematics | Institute for Advanced Study
Álvaro Pelayo, Michael A. Warren. Homotopy type theory and Voevodsky's univalent foundations. arXiv: https://arxiv.org/abs/1210.5658
See Ahrens, Benedikt; Kapulkin, Chris; Shulman, Michael (2015). "Univalent categories and the Rezk completion". Mathematical Structures in Computer Science. 25 (5): 1010–1039. arXiv:1303.0584. doi:10.1017/S0960129514000486. S2CID 1135785.
Univalent foundations and the equivalence principle - Benedikt Ahrens
https://www.youtube.com/watch?v=okx4Uklvwco